perm filename NEGATE.NEW[1,JRA]2 blob
sn#030162 filedate 1973-03-16 generic text, type T, neo UTF8
00100
00200
00300 (DEFPROP NEGATE
00400 (LAMBDA(Z)
00500 (PROG (BDY)
00700 (COND ((EQ (LENGTH Z) 1) (SETQ BDY (FIXNEG (CAR Z))) (GO D)))
00800 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CADR Z)) (FIXNEG (CAR Z))))
00900 (SETQ Z (CDDR Z))
01000 C (COND ((NULL Z) (GO D)))
01100 (SETQ BDY (LIST (QUOTE OR) (FIXNEG (CAR Z)) BDY))
01200 (SETQ Z (CDR Z))
01300 (GO C)
01400 D (RETURN (SET3 (SETUP (CNF (LIST (QUOTE NOT) (FIXQFF BDY))))))))
01500 EXPR)
01600
01700 (DEFPROP UPDATE
01800 (LAMBDA(E)
01900 (PROG (USINGFL USING
02000 CHAN1
02100 ELOC
02200 CHAN
02300 AUTO
02400 DL1
02500 RF
02600 XYZ
02700 XYZ1
02800 CMD
02900 LOCFLG
03000 Z
03100 Z1
03200 Z2
03300 INCT
03400 Z3
03500 UEX
03600 Z1R
03700 Z2R
03800 N1
03900 R
04000 N
04100 NAME
04200 NAMELIST
04300 ZZ)
04400 (SETQ CHAN (OUTC NIL NIL))
04500 (SETQ AXNO (QUOTE INSERT))
04600 (SETQ FNNAM (QUOTE EDI))
04700 (SETQ NAMELIST (CONS (CONS (QUOTE CLAUSES) E) (CONS (CONS (QUOTE DLIST) DLIST) NEWNAME)))
04800 (SETQ N1 (LAST NAMELIST))
04900 (SETQ INCT (INC NIL))
05000 U9 (SETQ ELOC E)
05100 (SETQ N 1)
05200 U3 (UP1A (CAR ELOC) N)
05300 U3A (TERPRI)
05400 U3AA (SETQ CMD (READ))
05500 (COND ((EQ CMD (QUOTE ;)) (GO U3AA)))
05600 U3B (COND ((NOT (ATOM CMD)) (GO UER2)))
05700 U3C (SETQ CMD (EXPLODE CMD))
05800 (COND ((EQ (LENGTH CMD) 1) (GO UER1))
05900 ((SETQ Z (ASSOC (READLIST (LIST (CAR CMD) (CADR CMD))) GOLIST)) (GO (CDR Z))))
06000 UER1 (PRINT (QUOTE ILLEGAL-COMMAND))
06100 (GO U3A)
06200 UER2 (PRINT (QUOTE IMPROPER-SYNTAX))
06300 (GO U3A)
06400 UDI1 (SETQ Z1 (UPGETL E NAMELIST))
06500 (COND ((NULL Z1) (GO U3A)))
06600 (CLAUSES Z1)
06700 (GO U3A)
06800 USY1 (PRINT (QUOTE THE-ENTRIES-ARE:))
06900 (SETQ Z NAMELIST)
07000 USY2 (COND ((MEMQ (CAAR Z) (QUOTE (NIL %% %INITIAL %USING))) NIL) (T (PRINT (CAAR Z))))
07100 (SETQ Z (CDR Z))
07200 (COND (Z (GO USY2)))
07300 (GO U3A)
07400 UFL2 (SETQ Z (QUOTE U))
07500 (GO UFL4)
07600 UFL3 (SETQ Z (QUOTE D))
07700 (GO UFL4)
07800 UFL1 (SETQ Z (CAR (EXPLODE (READ))))
07900 UFL4 (SETQ Z2 405104)
08000 (COND ((EQ Z (QUOTE U)) (GO U8)) ((EQ Z (QUOTE D)) (GO U7)) (T (GO UER1)))
08100 UCH1 (SETQ Z (SETQUERY1 (CONS NIL CLAUSES) STRAT))
08200 (COND ((OR (NULL Z) (EQ (CAR Z) (QUOTE ABORT))) (GO U3A)))
08300 (UPDATESTATE (CDDR Z))
08400 (GO U3A)
08500 UDE1 (SETQ Z2 (UPGETL E NAMELIST))
08600 (COND ((NULL Z2) (GO U3A)))
08700 (EXPUNGE Z2)
08800 (GO U3A)
08900 UIN1 (SETQ NAME (READ))
09000 (SETQ Z2 (UPGETL E NAMELIST))
09100 (COND ((NULL Z2) (GO U3A)))
09200 UIN1A
09300 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) NIL) (T (GO USE2)))
09400 (NCONC Z1 Z2)
09500 (GO U3A)
09600 USU1 (SETQ Z1 (ERRSET (GETTERMS)))
09700 (COND ((NULL Z1) (PRINT (QUOTE HACK-IN-SUBSTITUTION-RETURNING-TO-LISTEN-LOOP)) (GO U3A))
09800 ((NULL (CAR Z1)) (GO U3A)))
09900 (SETQ Z3 NIL)
10000 (SETQ Z1 (CAR Z1))
10100 USU2 (SETQ Z3 (CONS (SUBST1 XYZ XYZ1 (CDAR Z1)) Z3))
10200 (SETQ Z1 (CDR Z1))
10300 (COND (Z1 (GO USU2)) (T (SETQ NAME (QUOTE ASSERT)) (SETQ Z2 (SETUP Z3)) (GO UIN1A)))
10400 UUP1(SETQ Z2(READ))
10500 (COND((AND(NUMBERP Z2)(EQ(READ) @;))(GO U8))(T(GO UER2)))
10600 UDO1(SETQ Z2(READ))
10700 (COND((AND(NUMBERP Z2)(EQ(READ)@;))(GO U7))(T(GO UER2)))
10800 UAN1 (SETQ Z2 (UPGETL E NAMELIST))
10900 UAN2 (COND (Z2 (PROOF1 (CAR Z2))) (T (GO U3A)))
11000 (SETQ Z2 (CDR Z2))
11100 (GO UAN2)
11200 UTE1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z NIL)) (T (SETQ Z (UPGETL E NAMELIST))))
11300 (INC INCT)
11400 (OUTC CHAN NIL)
11500 (SETQ DLIST (GETNAME (QUOTE DLIST) NAMELIST))
11600 (SETQ Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))
11700 (RETURN (MINIMIZE (APPEND Z1 Z)))
11800 USA1 (SETQ Z2 (UPGETL E NAMELIST))
11900 (COND (Z2 (NCONC E Z2)))
12000 (GO U3A)
12100 UPA1 (SETQ Z1 (UPGETL E NAMELIST))
12200 (SETQ Z2 (UPGETL E NAMELIST))
12300 (COND ((AND Z1 Z2) (SETQ RF NIL) (GO URE1A)) (T (GO U3A)))
12400 USI1 (COND ((NULL (SETQ Z1 (UPGETL E NAMELIST))) (GO U3A)))
12500 (COND ((NOT (EQ (READ) (QUOTE BY))) (GO UER2)))
12600 (COND ((NULL (SETQ Z2 (UPGETL E NAMELIST))) (GO U3A)))
12700 (SETQ Z3 Z1)
12800 (SETQ Z DDEPTH)
12900 (SETQ DDEPTH 22)
13000 USI2 (DEMOD (LIST (CAR Z3)) Z2)
13100 (SETQ Z3 (CDR Z3))
13200 (COND (Z3 (GO USI2)))
13300 (PRINT (QUOTE CLAUSES-ARE:))
13400 (CLAUSES Z1)
13500 (SETQ DDEPTH Z)
13600 (GO U3A)
13700 UAS1 (SETQ NAME (QUOTE ASSUMPTIONS))
13800 (GO UUS3)
13900 UCU1 (QUERY)
14000 (GO U3A)
14100 UDS1 (SETQ Z1 (READ))
14200 (COND ((NOT (ATOM Z1)) (GO UDS3)))
14300 UDS2 (COND
14400 ((EQ (CAR (SETQ Z2 (REVERSE (EXPLODE Z1)))) (QUOTE ;)) (SETQ Z1 (READLIST (REVERSE (CDR Z2))))
14500 (GO UDS2)))
14600 UDS3 (SETQ CHAN1 (EVAL (LIST (QUOTE OUTC) (LIST (QUOTE OUTPUT) (QUOTE EDIT) (QUOTE DSK:) Z1) NIL)))
14700 (GO U3A)
14800 UEO1 (OUTC CHAN1 T)
14900 (GO U3A)
15000 UUS1 (SETQ NAME (QUOTE %USING))
15100 (SETQ USINGFL T)
15200 (SETQ USING NIL)
15300 UUS3 (SETQ LOCFLG T)
15400 UUS2 (SETQ Z2 (UPGETL E NAMELIST))
15500 (SETQ USINGFL NIL)
15600 (COND ((NULL Z2) (GO U3A)))
15700 USE2 (COND ((SETQ Z1 (ASSOC NAME NAMELIST)) (RPLACD Z1 Z2)))
15800 (COND (LOCFLG (RPLACD NAMELIST (CONS (CONS NAME Z2) (CDR NAMELIST))))
15900 (T (RPLACA (CAR N1) NAME)
16000 (RPLACD (CAR N1) Z2)
16100 (RPLACD N1 (CONS (CONS NIL NIL) NIL))
16200 (SETQ N1 (CDR N1))))
16300 (GO U3A)
16400 USE1 (SETQ NAME (READ))
16500 (SETQ LOCFLG NIL)
16600 (GO UUS2)
16700 UCL1 (SETQ Z (READ))
16800 UCL2 (COND ((SETQ Z1 (ASSOC Z NAMELIST)) (RPLACA Z1 (QUOTE %%)) (GO U3A))
16900 ((EQ (CAR (SETQ Z (REVERSE (EXPLODE Z)))) (QUOTE ;)) (SETQ Z (READLIST (REVERSE (CDR Z))))
17000 (GO UCL2))
17100 (T (GO U3A)))
17200 UGO1 (SETQ Z1 (READ))
17300 (COND ((NOT (NUMBERP Z1)) (GO UER2)))
17400 (COND ((SETQ Z (DOWN Z1 E)) (SETQ ELOC Z) (SETQ N Z1) (GO U3))
17500 (T (PRINT (QUOTE NO-SUCH-CLAUSE)) (GO U3A)))
17600 UTR1 (SETQ UEX NIL)
17700 (GO UEX2)
17800 UEX1 (SETQ UEX T)
17900 UEX2 (SETQ NAME (QUOTE LEMMA))
18000 (SETQ XYZ (GETNAME (QUOTE NEGLEMMA) NAMELIST))
18100 (COND ((NULL XYZ) (PRINT (QUOTE NOTHING-TO-PROVE)) (GO U3A)))
18200 (SETQ AUTO T)
18300 (SETQ Z2
18400 (ATTEMPT (INITIALAX (CONS (QUOTE THEOREM) (APPEND XYZ USING)))
18500 (COND (UEX (RESET (DLIST (GETNAME (QUOTE DLIST) NAMELIST)) (STRATEGY (SUPPORT XYZ))))
18600 (T NIL))
18700 NIL))
18800 (SETQ AUTO NIL)
18900 (GO AT1A)
19000 UST1 (STOP)
19100 (GO U3A)
19200 UAB1 (COND ((EQ (CAR (LAST CMD)) (QUOTE ;)) (SETQ Z1 NIL)) (T (SETQ Z1 (UPGETL E NAMELIST))))
19300 (ERR (CONS (QUOTE ABORT) (CONS Z1 (GETNAME (QUOTE %INITIAL) NAMELIST))))
19400 U8 (COND ((EQ Z2 0) (GO U9)))
19500 U83 (COND ((NULL Z2) (GO U3A)) ((TTYIN) (GO U3A)) ((LESSP Z2 5) (SETQ ZZ Z2) (SETQ Z2 NIL) (GO U84)))
19600 (SETQ Z2 (DIFFERENCE Z2 5))
19700 (SETQ ZZ 5)
19800 U84 (SETQ Z N)
19900 (SETQ Z3 (DIFFERENCE N ZZ))
20000 (COND ((OR (ZEROP Z3) (MINUSP Z3)) (SETQ Z3 1) (SETQ Z2 NIL)))
20100 (SETQ N Z3)
20200 (SETQ Z3 ELOC)
20300 (SETQ ELOC (DOWN N E))
20400 (SETQ ZZ NIL)
20500 (SETQ Z1 ELOC)
20600 U81 (COND ((EQ Z1 Z3) (GO U82)))
20700 (SETQ ZZ (CONS (CAR Z1) ZZ))
20800 (SETQ Z1 (CDR Z1))
20900 (GO U81)
21000 U82 (COND ((NULL ZZ) (GO U83)))
21100 (UP1A (CAR ZZ) (SUB1 Z))
21200 (SETQ ZZ (CDR ZZ))
21300 (SETQ Z (SUB1 Z))
21400 (GO U82)
21500 U7 (COND ((ZEROP Z2) (SETQ ELOC (LAST ELOC)) (SETQ N (LENGTH E)) (GO U3)))
21600 (SETQ Z2 (PLUS Z2 N))
21700 U7A (COND ((NULL (CDR ELOC)) (PRINT (QUOTE END)) (GO U3A)))
21800 (SETQ ELOC (CDR ELOC))
21900 (SETQ N (ADD1 N))
22000 (UP1A (CAR ELOC) N)
22100 (COND ((EQ N Z2) (GO U3A)) ((TTYIN) (GO U3A)) (T (GO U7A)))
22200 UPR1 (TERPRI)
22250 (SETQ XYZ NIL)
22300 (SETQ Z2 (UPGETL E NAMELIST))
22400 (COND ((NULL Z2) (PRINT (QUOTE NO-CLAUSES-GIVEN)) (GO U3A)))
22500 (COND ((GREATERP (LENGTH Z2) 1) (PRINT (QUOTE MORE-THAN-ONE-CLAUSE-TAKING-THE-FIRST-ONE))))
22600 (SETQ AXNO (QUOTE THEOREM))
22700 (SETQ Z3(COND((NULL XYZ)(NEGATE (CDAR Z2)))(T
22750 (SET3(SETUP(CNF(LIST @NOT XYZ)))))))
22800 (SETQ AXNO (QUOTE INSERT))
22900 (SETQ Z1 (ASSOC (QUOTE NEGLEMMA) NAMELIST))
23000 (COND (Z1 (RPLACD Z1 Z3)) (T (RPLACD NAMELIST (CONS (CONS (QUOTE NEGLEMMA) Z3) (CDR NAMELIST)))))
23100 (SETQ NAME (QUOTE LEMMA))
23200 (SETQ LOCFLG T)
23300 (GO USE2)
23400 UME1 (SETQ Z1 (UPGETL E NAMELIST))
23500 (SETQ Z2 (UPGETL E NAMELIST))
23600 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
23700 (BAKSUB Z1 Z2)
23800 (GO U3A)
23900 UHE1 (PRINT MESSAGE)
24000 (GO U3A)
24100 URE1 (SETQ Z1 (UPGETL E NAMELIST))
24200 (SETQ Z2 (UPGETL E NAMELIST))
24300 U%RE1
24400 (SETQ RF T)
24500 URE1A
24600 (COND ((OR (NULL Z1) (NULL Z2)) (GO U3A)))
24700 (SETQ Z1R Z1)
24800 (SETQ Z2R Z2)
24900 (SETQ Z3 NIL)
25000 (COND ((OR (NULL Z1) (NULL Z2)) (GO UR3B)))
25100 (COND ((NOT RF) (SETQ DL1 DLIST) (SETQ DLIST NIL)))
25200 UR3 (COND ((AND RF (ALLPOS (CAR Z1R)) (ALLPOS (CAR Z2R))) (GO UR3A))
25300 ((AND (ALLNEG (CAR Z1R)) (ALLNEG (CAR Z2R))) (GO UR3A)))
25400 (COND (RF (SETQ R (RESOLVE (CAR Z1R) (CAR Z2R)))) (T (SETQ R (PARMOD (CAR Z1R) (CAR Z2R)))))
25500 (COND ((NULL R) (GO UR3A)) ((MEMQ NIL R) (PROOF (CAR Z1R) (CAR Z2R)) (GO U3A)))
25600 (SETQ Z3 (BOOKEEP Z3 R (CONS (CAR Z1R) (CAR Z2R))))
25700 UR3A (SETQ Z2R (CDR Z2R))
25800 (COND (Z2R (GO UR3)))
25900 (SETQ Z1R (CDR Z1R))
26000 (COND (Z1R (SETQ Z2R Z2) (GO UR3)))
26100 UR3B (COND ((NULL Z3)
26200 (COND (RF (PRINT (QUOTE NO-RESOLVENTS)) (GO U3A))
26300 (T (PRINT (QUOTE NO-PARMODULANTS)) (SETQ DLIST DL1) (GO U3A))))
26400 (RF (SETQ NAME (QUOTE RES)))
26500 (T (SETQ NAME (QUOTE PAR)) (SETQ DLIST DL1)))
26600 (SETQ Z2 Z3)
26700 (SETQ LOCFLG T)
26800 (GO AT2A)
26900 UEV1 (PRINT (QUOTE EVAL-AWAITS))
27000 (SETQ Z2 (ERRSET (EVAL (READ)) T))
27100 (COND (Z2 (PRINT (CAR Z2)) (GO UE2)) (T (PRINT (QUOTE LOSE)) (GO UEV1)))
27200 UE2 (COND ((EQ (QUOTE END) (CAR Z2)) (GO U3A)))
27300 (GO UEV1)
27400 AT1A (UPDATESTATE STRAT)
27500 (COND
27600 ((OR (NULL Z2) (AND (EQ (CAR Z2) (QUOTE ABORT)) (NULL (CADR Z2))))
27700 (PRINT (QUOTE ATTEMPT-ABORTED-FOR:))
27800 (PRINC NAME)
27900 (GO U3A))
28000 ((EQ (CAR Z2) (QUOTE NOPROOF)) (SETQ AUTO T)
28100 (SETQ Z2 (ATTEMPT (INITIALAX1 (CADR Z2)) (CDDR Z2) NIL))
28200 (SETQ AUTO NIL)
28300 (GO AT1A))
28400 ((EQ (CAR Z2) (QUOTE QED)) (PRINT (QUOTE PROOF-FOUND-FOR:)) (PRINC NAME) (GO U3A)))
28500 (SETQ Z2 (CADR Z2))
28600 AT2A (SETQ N 1)
28700 AT2 (COND ((ASSOC (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))) NAMELIST) (SETQ N (ADD1 N)) (GO AT2)))
28800 (SETQ NAME (READLIST (APPEND (EXPLODE NAME) (EXPLODE N))))
28900 (PRINT (QUOTE THE-PROVER-RETURNS-THE-FOLLOWING-LOVELY-CLAUSES:))
29000 (PRINT (QUOTE THEY-WILL-BE-FOUND-UNDER-THE-NAME:))
29100 (PRIN1 NAME)
29200 (CLAUSES Z2)
29300 (GO USE2)))
29400 EXPR)
29500
29600 (DEFPROP UPGETL1
29700 (LAMBDA(C E N)
29800 (PROG (N1 Z Z1 Z2 Z3 ZZ N2)
29900 AS1 (SETQ Z (CAR C))
30000 (COND ((ATOM Z)
30100 (COND ((NUMBERP Z) (SETQ N2 (QUOTE CLAUSES))
30200 (COND ((SETQ Z1 (DOWN Z E)) (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1)))))
30300 (T (RETURN NIL))))
30400 ((SETQ Z1 (GETNAME Z N)) (SETQ N2 Z) (SETQ ZZ (APPENDIT ZZ Z1)))
30500 (T (RETURN NIL))))
30600 ((EQ (CAR Z) (QUOTE STAT)) (GO AS10))
30700 ((EQ (CAR Z) (QUOTE FIND)) (GO AS20))
30800 ((EQ (CAR Z) (QUOTE DSK)) (GO AS30))
30900 ((SETQ Z1 (GETNAME (CAR Z) N)) (SETQ N2 (CAR Z)) (GO AS2))
31000 (T (RETURN NIL)))
31100 AS6 (SETQ C (CDR C))
31200 (COND (C (GO AS1)) (T (RETURN ZZ)))
31300 AS2 (SETQ Z2 (CADR Z))
31400 (SETQ N1 (CAR Z))
31500 (SETQ Z (CDR Z))
31600 (SETQ Z3 Z1)
31700 AS2A (COND ((NOT (NUMBERP Z2)) (PRINT (QUOTE NON-NUMERIC-ARG-FOR:)) (PRINC N1) (RETURN NIL)))
31800 AS3 (SETQ Z2 (SUB1 Z2))
31900 (COND ((ZEROP Z2) (GO AS4)))
32000 (SETQ Z1 (CDR Z1))
32100 (COND (Z1 (GO AS3)) (T (PRINT (QUOTE EXCEEDED-SIZE-OF:)) (PRINC N1) (RETURN NIL)))
32200 AS4 (COND
32300 ((NOT (HERE (CAR Z1))) (PRINT N1)
32400 (PRINC (QUOTE / ))
32500 (PRINC (CAR Z))
32600 (PRINC (QUOTE / ))
32700 (PRINC (QUOTE HAS-BEEN-DELETED))
32800 (RETURN NIL)))
32900 (SETQ ZZ (APPENDIT ZZ (LIST (CAR Z1))))
33000 (SETQ Z (CDR Z))
33100 (COND (Z (SETQ Z1 Z3) (SETQ Z2 (CAR Z)) (GO AS2A)))
33200 (GO AS6)
33300 AS10 (SETQ N2 (QUOTE INSERT))
33400 (SETQ ZZ (APPENDIT ZZ (SET3 (SETUP (CNF(COPY(SETQ XYZ (FIXQFF (CDR Z)))))))))
33500 (GO AS6)
33600 AS20 (SETQ N2 (QUOTE MATCHES))
33700 (SETQ Z (MAPIT (CADR Z) (LIST (QUOTE FUNCTION) (LIST (QUOTE LAMBDA) (QUOTE (C)) (CADDR Z))) N))
33800 (COND ((NULL Z) (GO AS6)) (T (GO AS31)))
33900 AS30 (SETQ N2 (QUOTE INPUT))
34000 (SETQ ZIN (CDR Z))
34100 (COND
34200 ((NULL (ERRSET (EVAL (LIST (QUOTE INPUT) (QUOTE DSK:) ZIN)))) (PRINT (QUOTE CONTINUING)) (GO AS6)))
34300 (INC T)
34400 (SETQ Z (INCLAUSES))
34500 (INC NIL)
34600 (COND ((NULL Z) (RETURN NIL)))
34700 AS31 (SETQ ZZ (APPENDIT ZZ Z))
34800 (GO AS6)))
34900 EXPR)